COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	MAKEPROOF ELEPHREV
C00004 ENDMK
C⊗;
MAKEPROOF ELEPHREV;
SWITCH TO ELEPHREV;

DECLARE OPCONST uuu(NATNUM) = LIST, vvv(NATNUM) = LIST, pc(NATNUM) = NATNUM;

DECLARE INDVAR t,t1 ε NATNUM;

AXIOM ELEPHREV:

pc(0) = 0

∀t.(uuu(t+1) = IF pc(t) = 0 THEN w
		ELSE IF pc(t) = 1 ∧ ¬NULL uuu(t) THEN cdr uuu(t)
		ELSE uuu(t))

∀t.(vvv(t+1) = IF pc(t) = 0 THEN qNIL
		ELSE IF pc(t) = 1 ∧ ¬NULL uuu(t) THEN cons(car uuu(t),vvv(t))
		ELSE vvv(t))

∀t.(pc(t+1)  = IF pc(t) = 1 ∧ ¬NULL uuu(t) THEN 1
		ELSE pc(t) + 1)
;;